package logicaDePredicados;


import java.util.Iterator;
import java.util.ArrayList;
import java.util.Arrays; 
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.ListIterator;
import java.util.Stack;





import exceptions.UnBalancedExpressionException;
import exceptions.UnDecidibleValueException;

public class QuantifierStrategy implements IParsingStrategy{

	private Sentence parsedSentence; 
	private Sentence postFixSentence;
	private PredicateConstant<?> values[];
	private HashMap<PredicateVariable<?>, Integer> indexMap; 
	private HashSet<ArrayList<PredicateConstant<?>>> combinatorialSet;
	public QuantifierStrategy (){
		postFixSentence=null;
		parsedSentence=null;
		indexMap= new HashMap<PredicateVariable<?>, Integer>(16);
		combinatorialSet= new HashSet<ArrayList<PredicateConstant<?>>>(500);
		
		
	}
	/**
	 * Parses and checks balance and decidability of the given sentence 
	 * @param sentence
	 * @return
	 * @throws UnBalancedExpressionException
	 * @throws UnDecidibleValueException
	 */
	public boolean parseSentence(Sentence sentence)throws UnBalancedExpressionException,UnDecidibleValueException{
		parsedSentence = sentence;
		if (checkBalance(sentence)){
			/**
			 * put the sentence in Prenex Normal Form
			 */
			toPrenexNormalForm();
			postFixSentence=toPostFix(parsedSentence);		
			
			/**
			 * validate the variables
			 */
			validateVariables(postFixSentence);
			return evaluate(postFixSentence);
			
		}else {
			throw new UnBalancedExpressionException ("unbalanced sentence");
		}

		//return uDoTheMath(postFixSentence);
	}
	/**
	 * Receives a sentences with predicates receiven constant parameters
	 * @param aPostFixSentence
	 * @return
	 * @throws UnBalancedExpressionException
	 * @throws UnDecidibleValueException
	 */
	private boolean uDoTheMath (Sentence aPostFixSentence) throws UnBalancedExpressionException, UnDecidibleValueException{
		Stack<Boolean> myStack = new Stack<Boolean>();
		Iterator <PredicateLogic> iterator = aPostFixSentence.getSentence().listIterator(getLastQuantifierIndex(aPostFixSentence)+1);
		PredicateLogic currentToken;
		while (iterator.hasNext()){
			currentToken=iterator.next();
			//if the token is an operand get its value and push it back to the stack
			if (isPredicate(currentToken)){
				PredicateLogic nextToken = iterator.next();
				if (nextToken.getClass().equals(PredicateConstant.class)){

					myStack.add(new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((PredicateConstant<?>)nextToken).getValue())));
				}
				if (nextToken.getClass().equals(PredicateVariable.class)){
					myStack.add(new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((PredicateVariable<?>)nextToken).getValue())));

				}
				/**
				 * if the parameter for the logic predicate is actually a Skolem Function, get the value of the function and therefore the value of the Logic predicate
				 */
				if (nextToken.getClass().equals(SkolemFunction.class)){
					/**
					 * get the next element, that should be either a constant or variable
					 */
					PredicateLogic skolemParameter = iterator.next();
					/**
					 * if it is a Variable, then treat it as one
					 */
					if (skolemParameter.getClass().equals(PredicateVariable.class)){  
						myStack.add (new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((SkolemFunction<?, ?>)nextToken).calculate(((PredicateVariable<?>)skolemParameter).getValue()))));
					}else {
						/**
						 * if it is a constant, then treat it as one
						 */
						if (skolemParameter.getClass().equals(PredicateConstant.class)){

							myStack.add (new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((SkolemFunction<?, ?>)nextToken).calculate(((PredicateConstant<?>)skolemParameter).getValue()))));
						}
						else{
							/**
							 * otherwise, somehow the sentence is screwed up, so throw an exception
							 */
							throw new UnBalancedExpressionException ("PredicateVariable or PredicateConstant needed after SkolemFunction");
						}
					}
				}
			}
			// if it is an operator pop the operands needed and push back the result, 
			if (currentToken.getClass().equals(LogicOperator.class)){
				if (currentToken.equals(LogicOperatorFactory.createNOT())){
					if (myStack.isEmpty()){
						throw new UnBalancedExpressionException ("wrong expression");

					}
					else{
						Boolean temp= myStack.pop();
						myStack.push(new Boolean(!temp.booleanValue()));
					}

				}
				else
				{
					if (myStack.size()<2){
						throw new UnBalancedExpressionException ("missing operands");
					}else {
						if (currentToken.equals(LogicOperatorFactory.createAND())){
							Boolean q = myStack.pop();
							Boolean p= myStack.pop();
							myStack.push(new Boolean(p.booleanValue()&&q.booleanValue()));
						}
						if (currentToken.equals(LogicOperatorFactory.createOR())){
							Boolean q = myStack.pop();
							Boolean p= myStack.pop();
							myStack.push(new Boolean(p.booleanValue()||q.booleanValue()));
						}


					}

				}
			}
		}
		boolean returnValue =myStack.pop().booleanValue();
		
		return returnValue;

	}
	/**
	 * returns true if the brackets are balanced or UnBalancedExpressionException if not.
	 * @param sentence
	 * @return
	 * @throws UnBalancedExpressionException
	 */
	private boolean checkBalance (Sentence sentence) throws UnBalancedExpressionException{
		int bracket=0;
		for (PredicateLogic i : sentence.getSentence()) {
			if (i.getName().equals(LogicOperatorFactory.createLeftBracket().getName())){
				bracket++;
			}
			if (i.getName().equals(LogicOperatorFactory.createRightBraket().getName())){
				bracket--;
			}
		}
		if (bracket!=0)
			throw new UnBalancedExpressionException ("Unbalanced Expression");
		return true;
	}

	/**
	 * converts the parsedSentence into prenex normal form
	 * @throws UnBalancedExpressionException 
	 */
	private void toPrenexNormalForm () throws UnBalancedExpressionException{

		int thenIndex = parsedSentence.indexOf(LogicOperatorFactory.createTHEN());
		if (thenIndex ==-1){
			
			return;
		}else {

			replaceThenWithConjunction(getLastQuantifierIndex(parsedSentence), parsedSentence.size()-1, thenIndex);
			replaceExistencialQuantifiers();
		}
		

	}
	/**
	 * replaces  "exists" with essential component and moves it to the beginning of the sentence if any
	 * @throws UnBalancedExpressionException 
	 */

	private void replaceExistencialQuantifiers () throws UnBalancedExpressionException{
		int existencialIndex=-1;
		PredicateLogic variable=null;
		if ((existencialIndex=parsedSentence.indexOf(LogicOperatorFactory.createExistentialQuantifier()))!=-1){
			parsedSentence.remove(existencialIndex);
			variable=parsedSentence.get(existencialIndex);
			parsedSentence.remove(existencialIndex);
			parsedSentence.add(existencialIndex,LogicOperatorFactory.createNOT());
			int toInsertIndex =getLastQuantifierIndex(parsedSentence);
			parsedSentence.add(toInsertIndex, LogicOperatorFactory.createEssentialQuantifier());
			if (variable.getClass()!=PredicateVariable.class){
				throw new UnBalancedExpressionException("Quantifiers must be followed by Variables");
			}
			parsedSentence.add(toInsertIndex+1,variable);

			replaceExistencialQuantifiers();
		}
	}
	/**
	 * returns the index where the next Essential quantifier should be placed
	 * Example:
	 * ForAll x ForAll y (DOG ( X ) ) -> ( MAMMAL(X)  )
	 *    
	 * returns 3
	 * @return
	 */
	private int getLastQuantifierIndex (Sentence sentence){
		ListIterator<PredicateLogic> iterator = sentence.getSentence().listIterator();
		PredicateLogic term= iterator.next();
		while (iterator.hasNext()&&term.equals(LogicOperatorFactory.createEssentialQuantifier())){
			if (term.equals(LogicOperatorFactory.createEssentialQuantifier())){
				term=iterator.next();

			}

			term=iterator.next();
		}
		if (iterator.hasNext()){
			
			return iterator.previousIndex();
		}
		return 0;
	}
	/**
	 * replaces -> at thenIndex with OR and negate first term, inside the specified scope 
	 * P -> Q == ¬P v Q
	 * 
	 * @param scopeBegin
	 * @param scopeEnd
	 * @param thenIndex
	 */
	private void replaceThenWithConjunction (int scopeBegin, int scopeEnd, int thenIndex){
		parsedSentence.add(thenIndex,LogicOperatorFactory.createRightBraket());
		thenIndex++;
		scopeEnd++;
		parsedSentence.getSentence().add(thenIndex+1,LogicOperatorFactory.createLeftBracket());
		scopeEnd++;
		
		parsedSentence.getSentence().remove(thenIndex);
		scopeEnd--;
		parsedSentence.getSentence().add(thenIndex,LogicOperatorFactory.createOR());
		scopeEnd++;
		parsedSentence.getSentence().add(scopeBegin,LogicOperatorFactory.createLeftBracket());
		scopeEnd++;
		parsedSentence.getSentence().add(scopeBegin,LogicOperatorFactory.createNOT());
		scopeEnd++;
		parsedSentence.getSentence().add(scopeEnd+1,LogicOperatorFactory.createRightBraket());
		scopeEnd++;
		parsedSentence.toString();
	}
	/**
	 * Converts the proposition to prefix without including any Quantifiers. Needs Prenex Form proposition to work
	 * @param inFixSentence
	 * @return
	 * @throws UnBalancedExpressionException
	 */
	private Sentence toPostFix(Sentence inFixSentence)throws UnBalancedExpressionException {
		Stack<PredicateLogic> myStack = new Stack<PredicateLogic>();
		Sentence postFix=new Sentence ();
		Sentence quantifiers = extractQuantifiers (inFixSentence);
		
		Iterator <PredicateLogic>iterator = inFixSentence.getSentence().listIterator(getLastQuantifierIndex(parsedSentence));
		while (iterator.hasNext()){
			try {

				PredicateLogic currentToken =  iterator.next();
				//If the token is an operand we simply add it to our answer.

				if (isOperand(currentToken)){

					postFix.add(currentToken);
					if (currentToken.getClass().equals(LogicPredicate.class)){
						postFix.add(iterator.next());
						
					}	

				}else {

					//If the token is an operator, and there's nothing else on our stack, we push that operator onto the stack. 
					if (currentToken.getClass().equals(LogicOperator.class) &&
							(!currentToken.equals(LogicOperatorFactory.createLeftBracket())||!currentToken.equals(LogicOperatorFactory.createLeftBracket()))&& myStack.isEmpty()){
						myStack.push(currentToken);

					}else {
						//If the token is a left parenthesis we simply push it onto the stack.
						if (currentToken.equals(LogicOperatorFactory.createLeftBracket()))
						{
							myStack.push(currentToken);

						}else{//operator is not a left parenthesis
							/**
							 * if the operator is a right parenthesis, we pop all the operators until the first left
							 * parenthesis. 
							 */
							if (currentToken.equals(LogicOperatorFactory.createRightBraket())){
								while (!myStack.peek().equals(LogicOperatorFactory.createLeftBracket())){

									postFix.add(myStack.pop());
									
								}
								myStack.pop();//pop the corresponding "(" 
							}else {
								/**
								 * If there is something on the stack, we compare the precedence of our current 
								 * operator with the one on the stack 
								 */
								if (!myStack.isEmpty()&&myStack.peek().equals(LogicOperatorFactory.createNOT())||currentToken.equals(LogicOperatorFactory.createNOT())){
									/**
									 * Handle unary operator before the rest of them
									 */

									if (currentToken.equals(LogicOperatorFactory.createNOT())){
										myStack.push(currentToken);


									}else {
										
									if (myStack.peek().equals(LogicOperatorFactory.createNOT())){
										postFix.add(myStack.pop());
										
										myStack.push(currentToken);
										
									}else
									{
										myStack.push(currentToken);


									}
									}

								}
							}
						}
					}
				}
			} catch (Exception e) {
				e.printStackTrace();
			}
		}
		while(! myStack.isEmpty()){
			postFix.add(myStack.pop());

		}
		/**
		 * join the quantifiers with the post fix notation expression
		 */
		quantifiers.addAll(postFix);
		return quantifiers;

	}
	/**
	 * Extracts the quantifiers and variables declaration from a sentence
	 * ForAllXForAlly �DOG(X)v�BIRD(y)vANIMAL(X)^�BIRD(X)^�MAMMAL(y)
	 * @param inFixSentence
	 * @return ForAll X ForAll y
	 */
	private Sentence extractQuantifiers(Sentence inFixSentence) {
		Sentence returnSentence = new Sentence();
		for (int i = 0; i <= getLastQuantifierIndex(inFixSentence); i++) {
			returnSentence.add(inFixSentence.get(i));
			
		}
		return returnSentence;
	}
	/**
	 * Determines if the element is an operand or not. An operand would be a unary or 2-ary predicate
	 * @param element
	 * @return
	 */
	private boolean isOperand (PredicateLogic element){
		return (!element.getClass().equals(LogicOperator.class)&&(!element.getClass().equals(LogicQuantifier.class)));
	}
	/**
	 * Returns true if the element is a Predicate, or false if otherwise
	 * @param element
	 * @return
	 */
	private boolean isPredicate (PredicateLogic element){
		return isOperand(element)&& element.getClass().equals(LogicPredicate.class);
	}
	/**
	 * Evaluates whether the element is an operator or not. NOTE: higher precedence operators should considered individually
	 * @param element
	 * @return 
	 */
	private boolean isOperator (PredicateLogic element){
		return (element.getClass().equals(LogicOperator.class)||element.getClass().equals(LogicQuantifier.class));
	}
	/**
	 * Evaluates a sentence that has quantifiers and the respective variables.
	 * @param postFixSentence 
	 * @return
	 * @throws UnBalancedExpressionException
	 * @throws UnDecidibleValueException
	 */
	private boolean evaluate (Sentence postFixSentence) throws UnBalancedExpressionException, UnDecidibleValueException{
		ArrayList<Pair<LogicPredicate<?>,PredicateVariable<?>>> pairedPredicates = new ArrayList<Pair<LogicPredicate<?>,PredicateVariable<?>>>();
		
		/*
		 * get the dependent predicates
		 */
		pairedPredicates= getDependentPredicates(postFixSentence);
		ArrayList<ArrayList<PredicateConstant<?>>> combinatorial =makeVariableValueList(pairedPredicates);
		/*
		 * instantiate the values array with the proper size 
		 */
		values= new PredicateConstant<?>[combinatorial.size()];
		combine(0,0,combinatorial);
		
		for (ArrayList<PredicateConstant<?>> combination : combinatorialSet) {
			Sentence finalValues = replaceVariables(postFixSentence, combination);
			boolean booleanValue = uDoTheMath(finalValues);
				if (!booleanValue){
					return false;
				}
		}
		
		
		
		return true;
	}
	
	
	/**
	 * Returns a collection with predicates paired to their variables. This should allow a combinatorial exploration of the possible values that a
	 * sentence can take.
	 * @param sentence
	 * @return
	 * @throws UnBalancedExpressionException
	 */
	@SuppressWarnings("unchecked")
	private ArrayList<Pair<LogicPredicate<?>,PredicateVariable<?>>> getDependentPredicates(Sentence sentence) throws UnBalancedExpressionException{
		
		ArrayList<Pair<LogicPredicate<?>,PredicateVariable<?>>> predicates = new ArrayList<Pair<LogicPredicate<?>,PredicateVariable<?>>>(5);
		/*
		 * start evaluating the sentence after the quantifiers
		 */
		for (ListIterator listIterator = sentence.getSentence().listIterator(getLastQuantifierIndex(sentence)+1); listIterator.hasNext();) {
			PredicateVariable<?> var;
			PredicateLogic element = (PredicateLogic)listIterator.next();
			/**
			 * if the element is a predicate
			 */
			if (isPredicate(element)){
				LogicPredicate<?> predicate = (LogicPredicate<?>)element;
				if (listIterator.hasNext()){
					/*
					 * get the corresponding variable 
					 */
					element= (PredicateLogic) listIterator.next();
					/*
					 * if the element is actually a variable, then the predicate is a dependent one.
					 * Given the case a predicate is affected by a skolem function then this predicate is no variable dependent
					 * so it does not have to be considered in the returned structure 
					 */
					if (element.getClass().equals(PredicateVariable.class)){
						
						var = (PredicateVariable<?>)element;
						Pair<LogicPredicate<?>,PredicateVariable<?>> pair = new Pair<LogicPredicate<?>, PredicateVariable<?>>(predicate,var);
						predicates.add(pair);
					} 
				} else {
				   throw new UnBalancedExpressionException ("sentence ends with predicate with no parameter");
				}
				
			}
			
		}
		return predicates;
	}
	/**
	 * Checks that the quantified variables are present in the sentence's body.
	 * @param sentence
	 * @throws UnBalancedExpressionException when there are quantified variables that not present in the sentence's body or viceversa
	 * 
	 */
	
	private void validateVariables(Sentence sentence) throws UnBalancedExpressionException{
		HashSet <PredicateVariable<?>> quantifiedVariables = new HashSet<PredicateVariable<?>>();
		HashSet <PredicateVariable<?>> variables= new HashSet<PredicateVariable<?>>();
		int i;
		/*
		 * get the quantified variables involved in the sentence
		 */
		for (i = 0; i <= getLastQuantifierIndex(sentence); i++) {
			if (sentence.get(i).getClass().equals(PredicateVariable.class)){
				PredicateVariable<?> var= (PredicateVariable<?>)sentence.get(i);
				quantifiedVariables.add(var);
				
			}
		}
		/*
		 * get the variables assigned to predicates or skolem functions
		 */
		
		for (Iterator<PredicateLogic> iterator = sentence.getSentence().listIterator(i); iterator.hasNext();) {
			PredicateLogic element = iterator.next();
			
			if (element.getClass().equals(PredicateVariable.class)){
				
				variables.add((PredicateVariable<?>)element);
				
			}
		}
		/*
		 * find out if the all the variables found in the sentence body are being quantified
		 */
		if (!quantifiedVariables.containsAll(variables)){
			
			/*
			 * if not, throw exception. The sentence is not well formed
			 */
			throw new UnBalancedExpressionException("Sentence contains variables that are not affected by any quantifier");
		}else {
			if (!variables.containsAll(quantifiedVariables)){
				throw new UnBalancedExpressionException ("Sentence contains quantified variables that are not used in it's body");
			}
		}
		
	}
	/**
	 * Makes the list of variables that will be exploited by the combinatorial generator. Also generates the index map that will be used to generate 
	 * the combinations.
	 * This method contemplates the possibility that a knowledge base is not fully decidable. This means that given certain 
	 * sentences which have several predicates depending on one variable, the latter might take values that are not 
	 * present in the maps of certain predicates they are applied to. This is validated during evaluation. 
	 * @param pairedPredicates
	 * @return hard to say what it is
	 */
	private ArrayList<ArrayList<PredicateConstant<?>>> makeVariableValueList (ArrayList<Pair<LogicPredicate<?>,PredicateVariable<?>>> pairedPredicates){
		
		ArrayList<ArrayList<PredicateConstant<?>>> returnStructure = new ArrayList<ArrayList<PredicateConstant<?>>>();
		
		
		for (Pair<LogicPredicate<?>,PredicateVariable<?>> pair : pairedPredicates) {
			/*
			 * if the variable has no index, we are adding the possible values for the first time.
			 */
			if (!indexMap.containsKey(pair.getSecondArgument())){
				indexMap.put(pair.getSecondArgument(), returnStructure.size());
				
				ArrayList<PredicateConstant<?>> valueList = new ArrayList<PredicateConstant<?>>();
				valueList.addAll(pair.getFirstArgument().getValueList());
				returnStructure.add(valueList);
			}else {
				
				int index= indexMap.get(pair.getSecondArgument()).intValue();
				
				HashSet<PredicateConstant<?>> valueSet = new HashSet<PredicateConstant<?>>();
				/*
				 * add the new values
				 */
				valueSet.addAll(pair.getFirstArgument().getValueList());
				/*
				 *add the values that were already in the structure 
				 */
                               
                                valueSet.addAll(returnStructure.get(index));
				returnStructure.get(index).clear();
				returnStructure.get(index).addAll(valueSet);
					
			}
						
		}
		return returnStructure;
		
	}
	/**
	 * Recursively generates all the possible combinations that a variable can take from it's dependent predicates
	 * @param i
	 * @param c
	 * @param combinatorial
	 */
	private void combine ( int i,int c, ArrayList<ArrayList<PredicateConstant<?>>> combinatorial) {
		if (i>=combinatorial.size()|| c>=combinatorial.get(i).size())
			return;
		int j;
		for (j = 0; j < combinatorial.get(i).size(); j++) {
			
			values[i]= combinatorial.get(i).get(j);
			combine (i+1,c+1,combinatorial);
		
			addToCombinatorialSet(values.clone());
		}
			
		
	}
	/**
	 * adds the current combination to the Combinatorial Set
	 * @param values
	 */
	private void addToCombinatorialSet(PredicateConstant<?> values[]){
		 
		ArrayList<PredicateConstant<?>> list = new ArrayList<PredicateConstant<?>>(); 
		
		list.addAll(Arrays.asList(values));
		combinatorialSet.add(list);
		
	}
	/**
	 * Replaces the generic variables in the sentence for actual values
	 * If the sentence is:
	 * ForAllX ForAlly �DOG(X)v�BIRD(y)vANIMAL(X)^�BIRD(X)^�MAMMAL(y)
	 * and Combination is x=pitbull and y=pidgeon
	 * @param targetSentence
	 * @param combination
	 * @return ForAllXForAlly�DOG(pitbull)v�BIRD(pitbull)vANIMAL(pitbull)^�BIRD(pitbull)^�MAMMAL(pitbull)
	 * @throws UnBalancedExpressionException 
	 */
	private Sentence replaceVariables (Sentence targetSentence, ArrayList<PredicateConstant<?>> combination) throws UnBalancedExpressionException{
		Sentence returnSentence= targetSentence.clone();
		
		
		int afterQuantifierIndex = getLastQuantifierIndex(returnSentence)+1;
		
		for (ListIterator<PredicateLogic> listIterator = returnSentence.getSentence().listIterator(afterQuantifierIndex); listIterator.hasNext();) {
			
			PredicateLogic element = listIterator.next();
			/*
			 * if the element is a variable, then get the index from the map and establish new value
			 */
			if (element.getClass().equals(PredicateVariable.class)){
				if (indexMap.containsKey(element)){
					((PredicateVariable<?>)element).setValue(combination.get(indexMap.get(element).intValue()).getValue());
								
					
				}else {
					throw new UnBalancedExpressionException ("misplaced variable"+element.toString()+" found. ");
				}
					
				
			}
			
		}
		return returnSentence;
	}
	
}
